#ifndef __SOLVER_CONSTANT_H__
#define __SOLVER_CONSTANT_H__

#include "cuda.h"
#include "cuda_runtime.h"
#include "device_launch_parameters.h"
#ifdef RANDOM_POLARITY
	#include "curand_kernel.h"
#endif

#include "global.h"
#include "clause.h"
#include "vec.h"

const std::string	__seed = "7777";

#ifdef RANDOM_POLARITY
	const unsigned long long	__curandSeed = 7777ULL;
#endif

const int			__maxRestart = 100;
// __threadsPerBlock should be greater than 32 and less than 1024 (better in multiple of warp size);
// 256 is better for distribution among CUDA cores.
const int			__threadsPerBlock = 32; // unknown synchronization bug if more than 32 threads (one warp).
const int			__threadsPerBlock2 = 32; // unknown synchronization bug if more than 32 threads (one warp).
// the CUDA limit of __blocksPerGrid is 65535;
// For GTX480, it has 15*32 = 480 CUDA cores, should be in multiple of 15.
// But it seems one multi-processor could execute only 8 blocks at the same time.
const int			__blocksPerGrid = 2;

// Launch bounds for compiler.
//const int			__minBlocksPerMultiprocessor = 4;

// Default stack limit size is 1024 bytes.
const unsigned int	__deviceStackSizeLimit = 1024;
const float			__deviceHeapSizeFraction = 0.95f;
const int			__clausePtrIndexCapacity = 256 * 1024; // 256k learnt + problem clauses.

// Solver parameters.
const unsigned int	__initialConflictLimit = 100;
const float			__claActivityDecayRate = 0.999f;

// These constant variables should not be dependent on the thread IDs.
// Constant memory size is 64 kB.

__device__ __constant__ int				__dev_initialLearntClauseLimit;
__device__ __constant__ float			__dev_claActivityIncreaseRate;
__device__ __constant__ int				__dev_unitClaArrSize;
__device__ __constant__ int				__dev_claArrSize;
__device__ __constant__ int				__dev_claArrIndexSize;
__device__ __constant__ int				__dev_varNumber;
__device__ __constant__ int				__dev_litNumber;
__device__ __constant__ int				__dev_unitClaNumber;
__device__ __constant__ int				__dev_claNumber;
__device__ __constant__ int				__dev_watchNumber;

__device__ __constant__ Lit*			__dev_unitClaArr;
__device__ __constant__ Lit*			__dev_claArr;
__device__ __constant__ int*			__dev_claArrIndex;
__device__ __constant__ Lbool*			__dev_varAssignment;
__device__ __constant__ int*			__dev_varOrder;
__device__ __constant__ Lit**			__dev_watchPointer;
__device__ __constant__ Lit*			__dev_trail;
__device__ __constant__ int*			__dev_decisionLevel;
__device__ __constant__ bool*			__dev_varSeenMarker;
__device__ __constant__ Clause**		__dev_antecedentPointer;

__device__ __constant__ unsigned int*	__dev_conflictCount;
__device__ __constant__ unsigned int*	__dev_decisionCount;
__device__ __constant__ unsigned int*	__dev_propagationCount;
__device__ __constant__ unsigned int*	__dev_conflictLitCount;
__device__ __constant__ Lbool*			__dev_satResult;

#ifdef RANDOM_POLARITY
	__device__ __constant__ curandState*	__dev_randState;
#endif

__device__ __constant__ unsigned int	__dev_varAssignmentPitch;
__device__ __constant__ unsigned int	__dev_varOrderPitch;
__device__ __constant__ unsigned int	__dev_watchPointerPitch;
__device__ __constant__ unsigned int	__dev_trailPitch;
__device__ __constant__ unsigned int	__dev_decisionLevelPitch;
__device__ __constant__ unsigned int	__dev_varSeenMarkerPitch;
__device__ __constant__ unsigned int	__dev_antecedentPointerPitch;

__device__ __constant__ Lit*			__dev_unitClauseLit;
__device__ __constant__ int*			__dev_unitVar;
__device__ __constant__ Clause**		__dev_clausePtrIndex;
__device__ __constant__ float*			__dev_clauseActivityKey;
__device__ __constant__ int*			__dev_clausePtrIndexSize;

__device__ __constant__ Vec <Lit>**		__dev_localUnitClausePtr;
__device__ __constant__ Vec <int>**		__dev_decisionLevelVarOrderPtr; // For back-tracking.
__device__ __constant__ Vec <int>**		__dev_decisionLevelTrailIdPtr; // For back-tracking.
__device__ __constant__ Vec <Lit>**		__dev_propagationQueuePtr;
__device__ __constant__ Vec <Lit>**		__dev_tempQueuePtr;
__device__ __constant__ Vec <Clause*>**	__dev_antecedentQueuePtr;
__device__ __constant__ Vec <Clause*>**	__dev_tempAntecedentPtr;
__device__ __constant__ Vec <Clause*>**	__dev_tempWatchListPtr;
__device__ __constant__ Vec <Lit>**		__dev_learntClauseLitPtr;

// __dev_watchList is allocated by device kernels.
__device__ __constant__ Vec <Clause*>**	__dev_watchList;

// Global variables on device.
__device__ int							__dev_hasResult;
#ifdef HALF_IDLE_BLOCK
	__device__ int							__dev_idleBlockCount;
#endif
__device__ unsigned int					__dev_conflictLimit;
#ifndef KEEP_LEARNT_CLAUSE
	__device__ unsigned int					__dev_learntClauseLimit;
#endif
__device__ float						__dev_claActivityIncreaseDelta;
__device__ int							__dev_decreaseClauseActivity;
__device__ int							__dev_unitClauseLitSize;

#endif /* __SOLVER_CONSTANT_H__ */
